CHOICE-STRATEGY-IS: 
SUPPORT[29,12,15]∧ANCESTRY∧EQUALITY[=,2];

EDIT-STRATEGY-IS: 
DEPTH[2]∨LENGTH[2];

ELAPSED-TIME =102419

NIL 1 2
1 I < X⊃I0 ≤ X;3 4
2 X <(2 * X);AXIOM
3 I ≤ X⊃I0 ≤ X;5 6
4 X < Y⊃X ≤ Y;AXIOM
5 X ≤ Z∧Z ≤ Y⊃X ≤ Y;AXIOM
6 I0 ≤ I;AXIOM